feat: Support for the {:opaque} attibute on const
#2545
Conversation
module X {
const {:opaque} x := 3
}
const {:opaque} x := 3
function {:opaque} f(i: int): int { i + 1 }
lemma L()
ensures f(2) == 3
{
reveal f();
reveal x;
} |
Test/dafny0/OpaqueConstants.dfy
Outdated
|
|
||
| module Module { | ||
| module M { | ||
| const {:opaque} Five := 5; |
There was a problem hiding this comment.
The semi-colon at the end of the line is not needed.
Test/dafny0/OpaqueConstants.dfy
Outdated
| assert M.Five == 5; // error: this is not known here | ||
| reveal M.Five; | ||
| assert M.Five == 5; |
There was a problem hiding this comment.
This test might not have the effect you think. If you assert something twice, I expect Dafny to complain only about the first assert. This is because Dafny's semantics of assert allows it to implicitly assume the condition after the assert. So, if you remove the reveal, you probably will still get just one verification error.
Instead, I suggest that you create two paths through your method:
if * {
assert M.Five == 5;
} else {
reveal M.Five;
assert M.Five == 5;
}or
if
case true =>
assert M.Five == 5;
case true =>
reveal M.Five;
assert M.Five == 5;| Twostate-Resolution.dfy(481,11): Error: expression is not allowed to invoke a lemma (reveal_OrdinaryOpaque) | ||
| Twostate-Resolution.dfy(481,11): Error: to reveal a function (OrdinaryOpaque), append parentheses |
There was a problem hiding this comment.
The test file (Twostate-Resolution.dfy) still has comments like (admittedly, a poor error message). Please remove those now, since your error messages are good.
Source/Dafny/Verifier/Translator.cs
Outdated
| @@ -6575,7 +6575,9 @@ AND Apply(f,h0,bxs) == Apply(f,h0,bxs) | |||
| var cf = (ConstantField)f; | |||
| if (cf.Rhs != null && RevealedInScope(cf)) { | |||
| var etran = new ExpressionTranslator(this, predef, NewOneHeapExpr(f.tok)); | |||
| sink.AddTopLevelDeclaration(ff.CreateDefinitionAxiom(etran.TrExpr(cf.Rhs))); | |||
| if (!Attributes.Contains(cf.Attributes, "opaque")) { | |||
There was a problem hiding this comment.
The Translator has a method IsOpaqueFunction, which checks if a function is opaque. I suggest you define an analogous method for constants and use it here. Alternatively, change the current IsOpaqueFunction to have the name IsOpaque and take any member declaration.
Source/Dafny/Rewriter.cs
Outdated
| List<MemberDecl> newDecls = new List<MemberDecl>(); | ||
| foreach (MemberDecl member in c.Members) { | ||
| if (member is ConstantField constant) { | ||
| if (!Attributes.Contains(constant.Attributes, "opaque")) { |
There was a problem hiding this comment.
See my comments in Translator.cs about having a method IsOpaque. I guess such a method can be defined in DafnyAst.cs or Resolver.cs instead of in Translator.cs.
There was a problem hiding this comment.
I didn't add it yet, but could add it to MemberDecl.
Source/Dafny/Rewriter.cs
Outdated
| Attributes lemma_attrs = new Attributes("auto_generated", new List<Expression>(), null); | ||
| lemma_attrs = new Attributes("opaque_reveal", new List<Expression>(), lemma_attrs); | ||
| lemma_attrs = new Attributes("verify", new List<Expression>() { new LiteralExpr(c.tok, false) }, lemma_attrs); |
There was a problem hiding this comment.
I suspect something similar is done for opaque functions. Can the code be shared?
Source/Dafny/Resolver.cs
Outdated
| ResolveNameSegment(expr as NameSegment, true, null, revealResolutionContext, true); | ||
| } else { | ||
| ResolveDotSuffix(expr as ExprDotName, true, null, revealResolutionContext, true); |
There was a problem hiding this comment.
For expr as NameSegment and expr as ExprDotName, you expect that expr will have those respective types. In other words, you expect that the as will not return null. To indicate this in the program text, I suggest you instead use a cast: (NameSegment)expr and (ExprDotName)expr.
Source/Dafny/Resolver.cs
Outdated
| } | ||
| MemberSelectExpr callee = (MemberSelectExpr)((ConcreteSyntaxExpression)expr).ResolvedExpression; | ||
| if (callee == null) { | ||
| } else if ((callee.Member is Lemma or TwoStateLemma && Attributes.Contains(callee.Member.Attributes, "axiom"))) { |
There was a problem hiding this comment.
One of the outermost pair of parentheses is redundant.
Source/Dafny/Resolver.cs
Outdated
| rewriters.Add(new OpaqueConstRewriter(this.reporter)); | ||
| rewriters.Add(new OpaqueFunctionRewriter(this.reporter)); |
There was a problem hiding this comment.
I suggest combining these two rewriters into one OpaqueRewriter.
fabiomadge
changed the title
const {:opaque}{:opaque} attibute on const
fabiomadge
changed the title
{:opaque} attibute on const{:opaque} attibute on const
Fixes #1338.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.